%Por: Roberto Rama
%Nota: Hay que hacer el auxiliar procesarComandoAux referido al ejercicio 10. Ver como ejemplo el ejercicio 11(ya lo hice).
\begin{problema}[]{procesarMensajeTE}{t: TelCO, u: Usuario, r: SMS}{}
%Esto no se de donde lo saque, pero en el enunciado del TP 
	\requiere{u \in usuarios(t)}
	\requiere[numeroValido]{(\exists g \selec gateways(t)) nroDestino(r) ==
	numero(g)} %Lo agregu� porque OJO ! pod�amos romper un invariante 
	
	\medskip
	
	\modifica{t}
	
	\medskip
	
	\asegura{mismos(usuarios(pre(t)), usuarios(t))} %esta bien esto? No crea nuevos usuarios cuando no estan en la lista? - No. No creo. Fijate que te agregué el requiere de hecho. Laski
	
	\asegura[esIgualElHistorialDeLosOtrosUsuarios]{\\
	(\forall h \selec usuarios(t), h\not= u) mensajes(pre(t), h) == mensajes (t, h)
	}
	
	\asegura[historialUsuario]{\\
	(mensajes(pre(t), u) == mensajes (t, u)_{[0.. \longitud {mensajes(t,u)} - 1 )})
	\\ \ylogico (r == ultimoEnviadoSMS(t,u))
	}
	
	\asegura[restoIguales]{(\longitud{gateways(pre(t))} ==
	\longitud{gateways(g)})\\ \ylogico ((\forall g \selec gateways(pre(t)),
	numero(g) \not= nroDestino(r) )(\exists h \selec gateways(t)) g == h)  
	}
	\medskip
	
	\asegura[elDelNroDeDestinoSigueEstando]{\\
	(\exists j \selec gateways(t)) nroDestino(r) == numero(j)
	}
		
	\asegura[modificaGateway]{ 
	(esComando(pre(t), nroDestino(r), r) \ylogico participaDeAlguna(pre(t),
	nroDestino(r), u) \ylogico \\
	procesarComandoAux( dameGateway(t, nroDestino(r)), \\
	dameGateway(pre(t), nroDestino(r)), u, r, ultimoRecibidoSMS(t,u) ))\\
	\ologico 
 	\\(\neg esComando(pre(t), nroDestino(r), r) \ylogico procesarMensajesAux(
 	dameGateway(t, nroDestino(r)), \\ dameGateway(pre(t), nroDestino(r)), u, r, ultimoRecibidoSMS(t,u) ))
	}
		
	
\end{problema}

	\medskip
	
	\begin{aux}{esComando}{t: TelCO, n: Numero, r: SMS}{Bool}{
		damePalabras(texto(r))_0 \in comandos( dameGateway(t,n) )
	}
	\end{aux}
	
	\begin{aux}{dameGateway}{t: TelCO, n: Numero}{Gateway}{
		\comp{g}{g \selec gateways(t), numero(g) == n }_0
	}
	\end{aux}
	
	\begin{aux}{participaDeAlguna}{t: TelCO, n: Numero, u: Usuario}{Bool}{\\
		(\exists t \selec trivas(dameGateway(t,n))) u \in participantes(t)
	}
	\end{aux}
		
	\begin{aux}{ultimoRecibidoSMS}{t: TelCO, u: Usuario}{SMS}{
		cascabel(\comp{sgd(dr)}{dr \selec mensajes(t,u)})
	}
	\end{aux}
	
	\begin{aux}{ultimoEnviadoSMS}{t: TelCO, u: Usuario}{SMS}{
		cascabel(\comp{prm(dr)}{dr \selec mensajes(t,u)})
	}
	\end{aux}
	
	
	% Aprobado por Lea Lunes 26 de Septiembre. Alguien que chequee esto; yo creo
	% que as� est� bien, pero por las dudas. Saqu� las funciones de esemeeSes
	% entrantes y salientes porque no las us�bamos en ning�n momento. Le borr� el
	% par�metro r a ultimoEnviadoSMS y ultimoRecibidoSMS porque tampoco lo usaba y
	% agregu� las cl�usulas que faltaban. Tambi�n verifiqu� los par�ntesis, as� que
	% no creo que haga falta tocarlos.
	
	
	



